/* Benchmarks for the PointerC verifier. */

// list reversal

struct list
{
  int data;
  struct list* next;
};

/*@ let list(l) = (l==null) ||
  @               (({l}) && list(l->next))
  @ in  list (l)
  @ end
  @*/
struct list* reversal (struct list* l)
{
  struct list* p; // points to old list
  struct list* q; // temp pointer
  
  p = null;
  /*======================================*/
  /* Pit #1: if q is dangling, then the two 
   * if branches will give two different D sets:
   * one includes q, one does not.
   */
  // q = null;
  
   if (l==null)
   {
     return l;
   }
   else
   {
     p = l->next;
     l->next = null;
     q = p;
     while (p!=null) /*@ (({l} && {p,q}) && list(l->next) && list(q->next))
                       @   ||(({l}) && list(l->next) && {p, q}N)
                       @*/
     {
       q = p->next;
       p->next = l;
       l = p;
       p = q;
     }
     return l;
   }
}
/*@ 
  @*/



/*@ 
  @*/
int main ()
{
  print (99);
  return 0;
}
/*@ 
  @*/
